/**                   GNU GENERAL PUBLIC LICENSE
 *                       Version 3, 29 June 2007
 *
 * Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>
 * Everyone is permitted to copy and distribute verbatim copies
 * of this license document, but changing it is not allowed.
 * See License.txt file that comes with this distribution
 *
 *
 * Author: Vitaly German <vitaly.german@gmail.com>, (C) 2007
 * 
 **/

#include <iostream>
#include <stack>
#include <functional>
#include <string>
#include <cassert>

#if defined(BOOST_SPIRIT_DUMP_PARSETREE_AS_XML)
#include <map>
#endif

/// linear library 
#include "rlinear.h"

/// parser + solver's tree builder
#include "lr_calc.h"


using namespace std;
using namespace boost::spirit;

typedef char const*         iterator_t;
typedef tree_match<iterator_t> parse_tree_match_t;
typedef parse_tree_match_t::tree_iterator iter_t;



////////////////////////////////////////////////////////////////////////////
void math_test01();
void math_test02();
////////////////////////////////////////////////////////////////////////////
int
main()
{
  // look in tree_fcalc_grammar for the definition of calculator
  calculator calc;

  cout << "/////////////////////////////////////////////////////////\n\n";
  cout << "\t\tLinear Constraints Solver "<<"\n\n";
  cout << "/////////////////////////////////////////////////////////\n\n";
  cout << "Type an expression...or [q or Q] to quit\n\n";
  //std::cout<<"> "<<std::flush;

  string str;

  while (get_until(cin, str, ';'))
  {
   // if (!str.empty()) 
   // cout<<"\nOutput:-"<<str<<"-"<<endl;
    strip(str);
   //	if (!str.empty())
   //	cout<<"\nStripped:-"<<str<<"-"<<endl;
    if (str.empty() || str[0] == 'q' || str[0] == 'Q')
      break;

    tree_parse_info<> info = ast_parse(str.c_str(), calc, space_p);

    if (info.full)
    {
#if defined(BOOST_SPIRIT_DUMP_PARSETREE_AS_XML)
      // dump parse tree as XML
      std::map<parser_id, std::string> rule_names;

      rule_names[calculator::quantifierID] = "quantifier";
      rule_names[calculator::var_listID] = "var_list";
      rule_names[calculator::variableID] = "variable";

      rule_names[calculator::logicID] = "logic";
      rule_names[calculator::logic1ID] = "logic1";
      rule_names[calculator::logic2ID] = "logic2";

      rule_names[calculator::ltermID] = "lterm";
      rule_names[calculator::equsID] = "equs";

      rule_names[calculator::mathID] = "math";
      rule_names[calculator::mexprID] = "mexpr";
      rule_names[calculator::factorID] = "factor";
      rule_names[calculator::realID] = "real";

      tree_to_xml(cout, info.trees, str.c_str(), rule_names);
#endif

      // print the result
      /*
      cout << "parsing succeeded\n";
      cout << "evaluating \n " << evaluate(info) << "\n\n";
      cout << "transforming\n";
      */
     
      rfm_solver::debug("\n========= Tree: ==========\n");
#ifdef DEBUG
      prn(*info.trees.begin());
#endif
      rfm_solver::debug("\n");

      // tree_to_xml(cout, info.trees, str.c_str(), rule_names);
      // ConvertNode cn;
      // cn(*info.trees.begin());
      
      BuildFMERProblem build;
      try {
         Relation_aptr rel = build(*info.trees.begin());
		 cout<<"\nTree built: ";
         rel->print();
         rel->query_DNF();
         cout<<"\nSimplified: ";
         rel->print();
      } catch (NonlinearExprException&){
          cerr<<"\nInput formula is NOT linear one. "<<std::endl;
	  } catch (DivByZero & ex){
		  cerr<<"\nDivision by zero."<<std::endl;
	  } catch (std::exception & ex){
		  cerr<<"\nUnexpected exception caught: "<<ex.what()<<std::endl;
	  }
      
    }
    else
    {

	  cout << "parsing failed at:\n";
	  const char  end = '\0'; 
	  while(*info.stop!= end /* && *info.stop!='\n' */)
		cout<<*(info.stop++);
	  cout<<endl<<flush;
    }
  }
 
  cout << "Bye... :-) \n\n";
  return 0;
}

void math_test01() {
    using namespace rfm_solver;

    cout<<"\nSimplify Exists (x) (x >= 2 && -x >= -3 && a > 3) ";
    Relation_aptr rel = Relation::make();
    F_And_aptr fand = rel->add_and();
    F_Exists_aptr f(fand->add_exists());
    Variable_ID  x = f->declare("x");
    Variable_ID  a = rel->declare_free("a");

    F_And_aptr f_and ( f->add_and());

    Constraint_Handle handle (f_and->add_GEQ());
    handle.update_coef(x, 1);
    handle.update_const(2);

    handle = f_and->add_GEQ();
    handle.update_coef(x, -1);
    handle.update_const(-3);

    handle = f_and->add_GE();
    handle.update_coef(a, 1);
    handle.update_const(3);
    cout<<"\nInput: ";
    rel->print();
    DNF_aptr dnf= rel->query_DNF();
    cout<<"\nOutput: ";
    rel->print();

}

void math_test02() {
    using namespace rfm_solver;

    cout<<"\nSimplify (a >= 3) ";
    Relation_aptr rel = Relation::make();
    F_And_aptr f_and = rel->add_and();

  
    
    cout<<"\nOne var: ";
    rel->print();    
    F_And_aptr f_and1 = f_and->add_and();
    Constraint_Handle handle (f_and1->add_GE());
    
    Variable_ID  x = rel->declare_free("x");

    handle.update_coef(x, 1);
    handle.update_const(3);

    cout<<"\nInput: ";
    rel->print();
    DNF_aptr dnf= rel->query_DNF();
    cout<<"\nOutput: ";
    rel->print();

};
